$\forall$$A$:Type, ${\it eq}$:EqDecider($A$), $B$:($A$$\rightarrow$Type), $P$:($A$$\rightarrow\mathbb{B}$), $f$:$x$:$A$ fp$\rightarrow$ $B$($x$).
\\[0ex]fpf{-}vals(${\it eq}$;$P$;$f$) $\in$ ($x$:\{$a$:$A$$\mid$ $P$($a$) \}$\times$$B$($x$)) List